\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $k$:Knd, $l$:IdLnk, ${\it tg}$:Id, $n$:$\mathbb{N}$,\+
\\[0ex]$f$:(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$${\it da}$(rcv($l$,${\it tg}$))?Void).
\-\\[0ex]$k$ sends on $l$ with tag ${\it tg}$ [$s$,$v$.$f$($s$,$v$)], at marker $n$ $\in$ msg{-}spec(${\it ds}$;${\it da}$)
\end{tabbing}